/* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
 * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
 * merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
 * OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 */

package edu.mit.csail.sdg.alloy4whole;

import java.io.*;
import java.text.DecimalFormat;
import java.text.DecimalFormatSymbols;
import java.text.NumberFormat;
import java.util.*;

import kodkod.analysis.*;
import kodkod.analysis.AST.GraphVisitorDOT2;
import kodkod.analysis.AST.wClusteredGraph;
import kodkod.analysis.AST.wGraph;
import kodkod.analysis.AST.wNode;
import kodkod.analysis.ordering.*;
import kodkod.ast.Expression;
import kodkod.ast.Node;
import kodkod.ast.Relation;
import kodkod.ast.Formula;
import kodkod.instance.TupleSet;
import kodkod.util.ints.IntSet;
import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.CommandScope;
import edu.mit.csail.sdg.alloy4compiler.ast.Expr;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;

public final class AlloyBenchmark {
		
	private int numberOfRepeats = 1;
	
	private static final File input = new File("/home/markus/Diplomarbeit/BenchmarkModels3/");
	private static File outDirectory;
	private static ArrayList<File> files = new ArrayList<File>();
	private ArrayList<String> restrict = new ArrayList<String>();
	private ArrayList<String> exclude = new ArrayList<String>();
	
	private HashMap<String, Integer> bounds = new HashMap<String, Integer>();
	
	private static boolean performDefault = false;
	private static boolean performRestricted = false;
	private static boolean performUniform = true;
	private static boolean performSteplike = true;
		
	public AlloyBenchmark(File directory) {
		outDirectory = directory;
		
		if (!input.isDirectory()) {
			files.add(input);
		} else {
			files.addAll(getRecursive(input));
		}
/*		
		exclude.add("examples/algorithms/dijkstra DijkstraPreventsDeadlocks");
		exclude.add("examples/algorithms/dijkstra ShowDijkstra");
		exclude.add("examples/algorithms/opt_spantree BadLivenessTrace");
		exclude.add("examples/algorithms/opt_spantree Closure");
		exclude.add("examples/algorithms/opt_spantree SuccessfulRun");
		exclude.add("examples/algorithms/opt_spantree TraceWithoutLoop");
		exclude.add("examples/algorithms/peterson NotStuck");
		exclude.add("examples/algorithms/peterson Safety");
		exclude.add("examples/algorithms/peterson ThreeRun");
		exclude.add("examples/algorithms/peterson TwoRun");
		exclude.add("examples/algorithms/ringlead LeaderHighest");
		exclude.add("examples/algorithms/ringlead Liveness");
		exclude.add("examples/algorithms/ringlead NeverFindLeader");
		exclude.add("examples/algorithms/ringlead OneLeader");
		exclude.add("examples/algorithms/ringlead SomeLeader");
		exclude.add("examples/algorithms/stable_mutex_ring Closure");
		exclude.add("examples/algorithms/stable_mutex_ring TraceShorterThanMaxSimpleLoop");
		exclude.add("examples/algorithms/stable_mutex_ring TwoPrivileged");
		exclude.add("examples/algorithms/stable_orient_ring Closure");
		exclude.add("examples/algorithms/stable_orient_ring SomeState");
		exclude.add("examples/algorithms/stable_ringlead CBadLivenessTrace");
		exclude.add("examples/algorithms/stable_ringlead CMustConverge");
		exclude.add("examples/algorithms/stable_ringlead CTraceWithoutLoop");
		exclude.add("examples/algorithms/stable_ringlead ConvergingRun");
		exclude.add("examples/algorithms/stable_ringlead DBadLivenessTrace");
		exclude.add("examples/algorithms/stable_ringlead DTraceWithoutLoop");
		exclude.add("examples/case_studies/chord FindSuccessorWorks");
		exclude.add("examples/case_studies/chord InjectiveIds");
		exclude.add("examples/case_studies/chord Same1");
		exclude.add("examples/case_studies/chord Same2");
		exclude.add("examples/case_studies/chord SameCPF");
		exclude.add("examples/case_studies/chord SameCPF1");
		exclude.add("examples/case_studies/chord SameCPF2");
		exclude.add("examples/case_studies/chord SameFC");
		exclude.add("examples/case_studies/chord SameFP");
		exclude.add("examples/case_studies/chord SameFP1");
		exclude.add("examples/case_studies/chord SameFP2");
		exclude.add("examples/case_studies/chord ShowMe1");
		exclude.add("examples/case_studies/chord ShowMe1Node");
		exclude.add("examples/case_studies/chord ShowMe2");
		exclude.add("examples/case_studies/chord ShowMeCPF");
		exclude.add("examples/case_studies/chord ShowMeFC");
		exclude.add("examples/case_studies/chord2 FindSuccessorWorks");
		exclude.add("examples/case_studies/chordbug FindSuccessorWorks");
		exclude.add("examples/case_studies/chordbug ShowMe3");
		exclude.add("examples/case_studies/chordbug ShowMeCorrectSuccessorEg");
		exclude.add("examples/case_studies/chordbug StrongerFindSuccessorWorks");
		exclude.add("examples/case_studies/com Theorem1");
		exclude.add("examples/case_studies/com Theorem2");
		exclude.add("examples/case_studies/com Theorem3");
		exclude.add("examples/case_studies/com Theorem4a");
		exclude.add("examples/case_studies/com Theorem4b");
		exclude.add("examples/case_studies/firewire AtMostOneElected");
		exclude.add("examples/case_studies/firewire NoOverflow");
		exclude.add("examples/case_studies/iolus OutsiderCantRead");
		exclude.add("examples/case_studies/sync SyncSpecNotUnique");
		exclude.add("eunsuk/abstractFilesystem WriteIdempotent");
		exclude.add("eunsuk/abstractFilesystem WriteLocal");
		exclude.add("eunsuk/abstractFilesystem run$1");
		exclude.add("eunsuk/abstractFilesystem run$2");
		exclude.add("eunsuk/blockManager gcTest");
		exclude.add("eunsuk/consensusPaxos run$1");
		exclude.add("eunsuk/flash ProgramIdempotent");
		exclude.add("eunsuk/flash ProgramLocal");
		exclude.add("eunsuk/flash eraseSome");
		exclude.add("eunsuk/flash readSome");
		exclude.add("eunsuk/flash writeSome");
		exclude.add("eunsuk/naming WriteLocal");
		exclude.add("eunsuk/naming WriteRemoveConsistent");
		exclude.add("eunsuk/naming run$1");
		exclude.add("eunsuk/namingObject0 RenamePreservesStructure");
		exclude.add("eunsuk/namingObject0 RenameSamePath");
		exclude.add("eunsuk/namingObject0 remove");
		exclude.add("eunsuk/namingObject0 show_rename");
		exclude.add("eunsuk/namingObject0 write");
		exclude.add("eunsuk/Peterson2P MutualExclusionSatisfied");
		exclude.add("eunsuk/Peterson2P ProgressGuaranteed");
		exclude.add("eunsuk/Peterson2P run$1");
		exclude.add("eunsuk/planner run$1");
		exclude.add("examples/systems/javatypes TypeSoundness");
		exclude.add("examples/systems/lists reflexive");
		exclude.add("examples/systems/lists show");
		exclude.add("examples/systems/lists symmetric");
		exclude.add("examples/systems/marksweepgc Completeness");
		exclude.add("examples/systems/marksweepgc Soundness1");
		exclude.add("examples/systems/marksweepgc Soundness2");
		exclude.add("examples/systems/views zippishOK");
		exclude = new ArrayList();
 * 
 */
	}	
	
	private static ArrayList<File> getRecursive(File dir) {
		ArrayList<File> list = new ArrayList<File>();
		
		File[] files = dir.listFiles();
		Arrays.sort(files);
		for (File file : files) {
			if (file.canRead()) {
				if (file.isDirectory()) {
					list.addAll(getRecursive(file));
				} else if (file.getName().endsWith(".als")) {
					list.add(file);
				}
			}
		}
		
		return list;
	}

    public static void main(String[] args) throws Err {

    	File outDirectory = null;
    	
    	if (args.length < 1) {
    		System.err.println("Usage: AlloyBenchmark $OutputDirectory");
    		System.exit(-1);
    	} else {
    		outDirectory = new File(args[0]);
    		
    		if (!outDirectory.canWrite() || !outDirectory.isDirectory()) {
    			outDirectory = new File(System.getProperty("java.io.tmpdir"));
    		}
    	}
    	
    	AlloyBenchmark benchmark = new AlloyBenchmark(outDirectory);
    	benchmark.run();
    }
    
    public static PrintWriter getWriter(String prefix) {
    	String name = "benchmark";
    	if (files.size() == 1) {
    		name = files.get(0).getName().split("\\.")[0];
    	} else {
    		name = input.getName();
    	}
    	
    	File benchFile = new File(outDirectory, prefix+"."+name+".1.log");
    	
    	for (int i = 2; benchFile.exists(); i++) {
    		benchFile = new File(outDirectory, prefix+"."+name+"."+i+".log");
    	}
    	
    	PrintWriter out = null;

		try {
			out = new PrintWriter(benchFile);
		} catch (IOException ioe) {
			ioe.printStackTrace();
		}
    	
    	return out;
    }
    
    public static String readLine()	{
		String s = "";
		try {
			InputStreamReader converter = new InputStreamReader(System.in);
			BufferedReader in = new BufferedReader(converter);
			s = in.readLine();
		} catch (Exception e) {
			System.out.println("Error! Exception: "+e); 
		}
		return s;
	}
    
    private Command modifyBounds(Command command, int scope) {
    	return new Command(command.pos, command.label, command.check, scope, 
				command.bitwidth, command.maxseq, command.expects, new ArrayList<CommandScope>(), 
				command.additionalExactScopes, command.formula, command.parent);
    }
    
    public void run() throws Err {
//    	readLine();
    	
    	PrintWriter out = null;
    	
    	out = getWriter("_info");
    	
		for (File file : files) {
			Module module = CompUtil.parseEverything_fromFile(A4Reporter.NOP, null, file.getAbsolutePath());
							
			System.out.println("MODEL " + module.getModelName());
			
			class CommandComparator implements Comparator<Command> { 
				public int compare(Command o1, Command o2) {
					return o1.label.compareTo(o2.label);
				}
			}
			
			ArrayList<Command> commands = new ArrayList<Command>();
			commands.addAll(module.getAllCommands());
			Collections.sort(commands, new CommandComparator());
    		
	    	for (Command command: commands) 
	    	if ((restrict.size() == 0 || restrict.contains(module.getModelName() + " " + command.label))
	    			&& !exclude.contains(module.getModelName() + " " + command.label)) {
    			Problem problem = new Problem(module, command, new DefaultOrdering());
    			System.out.println(problem);
    			out.println(problem);
    			
    			Problem.skolemDepth = 0;
    			problem = new Problem(module, command, new DefaultOrdering());
    			benchmarkDefault(problem, out, "Skolem0-");
    			printInfo(problem, out);
    			
    			Problem.skolemDepth = 1;
    			problem = new Problem(module, command, new DefaultOrdering());
    			benchmarkDefault(problem, out, "Skolem1-");
    			printInfo(problem, out);
    			
    			Problem.skolemDepth = 2;
    			problem = new Problem(module, command, new DefaultOrdering());
    			benchmarkDefault(problem, out, "Skolem2-");
    			printInfo(problem, out);
    			
    			Problem.skolemDepth = 3;
    			problem = new Problem(module, command, new DefaultOrdering());
    			benchmarkDefault(problem, out, "Skolem3-");
    			printInfo(problem, out);
    			
    			Problem.skolemDepth = 4;
    			problem = new Problem(module, command, new DefaultOrdering());
    			benchmarkDefault(problem, out, "Skolem4-");
    			printInfo(problem, out);
    			
    			Problem.skolemDepth = 5;
    			problem = new Problem(module, command, new DefaultOrdering());
    			benchmarkDefault(problem, out, "Skolem5-");
    			printInfo(problem, out);
			}
		}		
		
		out.println("ENDE");
		out.close();
    }
    
    public void compareFuzziness(Module module, Command command, PrintWriter out) {
    	DecimalFormatSymbols symbols = new DecimalFormatSymbols();
		symbols.setDecimalSeparator('.');
		NumberFormat format = new DecimalFormat("#0.00", symbols);
		
		System.out.println(module.getModelName() + " " + command.label);
		out.print(module.getModelName().substring(module.getModelName().lastIndexOf('/')) + " " + command.label);
		out.print(" & ");
		Problem problem = new Problem(module, command, new DefaultOrdering());
		ExpressionAnalyzer.FUZZINESS = 0.01;
		Analyzer analyzer = new Analyzer(problem);
		ArrayList<Double> weights = analyzer.getRelationWeightsOrdered();
		out.print(format.format(weights.get(0)));
		out.print(" & ");
		ExpressionAnalyzer.FUZZINESS = 0.001;
		analyzer = new Analyzer(problem);
		weights = analyzer.getRelationWeightsOrdered();
		out.print(format.format(weights.get(0)));
		out.print(" \\\\");
		out.println();
    }
    
    public void boundsMaximization(Module module, Command command, PrintWriter out) throws Err {
		boolean defaultT = true;
		boolean restrictedT = true;
		boolean uniformT = true;
		boolean steplikeT = true;
		
		boolean done = false;
		boolean start = true;
		
		int minScope = command.scope.size() > 0 ? Integer.MAX_VALUE : 3;
		for (CommandScope scope : command.scope) {
			if (scope.endingScope < minScope) minScope = scope.endingScope;
		}
		
		System.out.println(module.getModelName() + " " + command.label);
		out.println(module.getModelName() + " " + command.label);
		
		int defaultMax = bounds.get(module.getModelName() + " " + command.label);
		if (defaultMax == 1) return;
		
		if (performDefault) {
			while (defaultT) {
				Command command2 = modifyBounds(command, defaultMax);
				Problem problem = new Problem(module, command2, new DefaultOrdering());
				System.out.println(command2);
				defaultT = benchmarkDefault(problem, out, "");
				
				if (defaultT) {
					if (!done && !start) {
						break;
					} else {
						done = true;
						defaultMax++;
					}
				} else {
					if (!done) {
						defaultT = true;
						defaultMax--;
					} else {
						defaultMax--;
						break;
					}
				}
				start = false;
			}
			out.println("defaultMaxScope: " + defaultMax);
			out.flush();
		}
		
		if (performRestricted) {
			int restrictedMax = defaultMax;
			while (restrictedT) {
				Command command2 = modifyBounds(command, restrictedMax);
				Problem problem = new Problem(module, command2, new DefaultOrdering());
				System.out.println(command2);
				restrictedT = benchmarkUniformOverride(problem, out);
				if (restrictedT) {
					if (restrictedMax < defaultMax) break;
					restrictedMax++;
				}
				else {
					if (restrictedMax <= defaultMax) restrictedT = true;
					restrictedMax--;
				}
			}
			out.println("restrictedMaxScope: " + restrictedMax);
			out.flush();
		}
		
		if (performUniform) {
			int uniformMax = defaultMax;
			while (uniformT) {
				Command command2 = modifyBounds(command, uniformMax);
				Problem problem = new Problem(module, command2, new DefaultOrdering());
				System.out.println(command2);
				uniformT = benchmarkUniformInitialize(problem, 3.0, out);
				if (uniformT) {
					if (uniformMax < defaultMax) break;
					uniformMax++;
				}
				else {
					if (uniformMax <= defaultMax) uniformT = true;
					uniformMax--;
				}
			}
			out.println("uniformMaxScope: " + uniformMax);
			out.flush();
		}
		
		if (performSteplike) {
			int steplikeMax = defaultMax;
			while (steplikeT) {
				Command command2 = modifyBounds(command, steplikeMax);
				Problem problem = new Problem(module, command2, new DefaultOrdering());
				System.out.println(command2);
				steplikeT = benchmarkSteplikeInitialize(problem, new Analyzer(problem), 2.0, 2.0, out);
				if (steplikeT) {
					if (steplikeMax < defaultMax) break;
					steplikeMax++;
				}
				else {
					if (steplikeMax <= defaultMax) steplikeT = true;
					steplikeMax--;
				}
			}
			out.println("steplikeMaxScope: " + steplikeMax);
			out.flush();
		}
    }
    
    public void printInfo(Problem problem, PrintWriter out) {
    	DecimalFormatSymbols symbols = new DecimalFormatSymbols();
		symbols.setDecimalSeparator('.');
		NumberFormat format = new DecimalFormat("#0.00", symbols);
		double cv = (double)problem.nClauses / (double)problem.nVars;
		double pv = (double)problem.nPrimaryVars / (double)problem.nVars;
		out.println("# " + problem.nClauses + " & " + problem.nVars + " & " + format.format(cv) + " & " + problem.nPrimaryVars + " & " + format.format(pv));
    }
    
    public void printRelationWeights(Analyzer analyzer, PrintWriter writer) throws Err {
    	ArrayList<LeafInfo> infos = new ArrayList<LeafInfo>(analyzer.leafInfos.values());
    	Collections.sort(infos);
		for (LeafInfo info : infos) {
			writer.println("#" + info);
		}
		writer.print("#");
		for (ArrayList<Integer> group : analyzer.getThreeGroups()) {
			for (int index : group) {
				writer.print(" " + index);
			}
			writer.print(";");
		}
		writer.println();
    }
    
    public void printBoundsExtension(Analyzer analysis, PrintWriter writer) {
    	for (Expression e : BoundsExtension.hash.keySet()) {
    		BoundsExtension be = BoundsExtension.hash.get(e);
    		writer.println(e);
    		writer.println("upper: " + be.upper);
    		writer.println("lower: " + be.lower);
    		writer.println();
    	}
    }
    
    public void graphAST(Problem problem, PrintWriter writer) throws Err {
    	wGraph.enableRemoveStaticPaths = false;
    	wGraph ast = new wGraph(problem);
		ast.printGraph(writer);
    }
    
    public void checkTime(Problem problem, PrintWriter out) throws Err { 
		Experiment experiment = new Experiment(problem, new DefaultOrdering());
		experiment.conduct(1);
		
		if (experiment.getTimeAverage() < 1000 || experiment.getTimeAverage() > 10000) {
			out.print(problem.toString());
			out.print(" " + experiment.getTimeAverage());
			out.println();
			out.flush();
		}
    }
    
    public boolean benchmarkDefault(Problem problem, PrintWriter out, String methodPrefix) throws Err { 
		DefaultOrdering ordering = new DefaultOrdering();
		
		System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		boolean notimeout = experiment.conduct(numberOfRepeats);
		
		if (out != null) {
			out.println(experiment.toString() + " Method:" + methodPrefix + ordering.toString());
			out.flush();
		}
		
		return notimeout;
    }
    
    public boolean benchmarkUniformOverride(Problem problem, PrintWriter out) throws Err { 
    	UniformPromotion ordering = new UniformPromotion();
    	ordering.softOrder = false;
    	
    	System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		boolean notimeout = experiment.conduct(numberOfRepeats);	
		
		out.println(experiment.toString() + " Method:" + ordering.toString());
		out.flush();
		
		return notimeout;
    }
    
    public boolean benchmarkUniformInitialize(Problem problem, double weight, PrintWriter out) throws Err { 
    	UniformPromotion ordering = new UniformPromotion(weight);
    	ordering.softOrder = true;
    	
    	System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		boolean notimeout = experiment.conduct(numberOfRepeats);	
		
		out.println(experiment.toString() + " Method:" + ordering.toString());
		out.flush();
		
		return notimeout;
    }
    
    public void benchmarkSoloOverride(Problem problem, Analyzer analyzer, PrintWriter out) throws Err {
    	SoloPromotion ordering = new SoloPromotion(analyzer);
    	ordering.softOrder = false;
    	
    	System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		experiment.conduct(numberOfRepeats);
		
		out.println(experiment.toString() + " Method:" + ordering.toString());
		out.flush();
    }
    
    public void benchmarkSoloInitialize(Problem problem, Analyzer analyzer, double weight, PrintWriter out) throws Err {
    	SoloPromotion ordering = new SoloPromotion(analyzer, weight);
    	ordering.softOrder = true;
    	
    	System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		experiment.conduct(numberOfRepeats);
		
		out.println(experiment.toString() + " Method:" + ordering.toString());
		out.flush();
    }
    
    public void benchmarkStackedInitialize(Problem problem, Analyzer analyzer, double weight1, double weight2, PrintWriter out) throws Err { 
		StackedPromotion ordering = new StackedPromotion(analyzer, weight1, weight2);
		ordering.softOrder = true;
		
		System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		experiment.conduct(numberOfRepeats);
		
		out.println(experiment.toString() + " Method:" + ordering.toString());
		out.flush();
    }
    
    public void benchmarkGroupStackedInitialize(Problem problem, Analyzer analyzer, double weight1, double weight2, PrintWriter out) throws Err { 
		GroupStackedPromotion ordering = new GroupStackedPromotion(analyzer, weight1, weight2);
		ordering.softOrder = true;
		
		System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		experiment.conduct(numberOfRepeats);
		
		out.println(experiment.toString() + " Method:" + ordering.toString());
		out.flush();
    }
    
    public boolean benchmarkSteplikeInitialize(Problem problem, Analyzer analyzer, double baseline, double factor, PrintWriter out) throws Err { 
		SteplikePromotion ordering = new SteplikePromotion(analyzer, baseline, factor);
		ordering.softOrder = true;
		
		System.out.println(ordering);
		
		Experiment experiment = new Experiment(problem, ordering);
		boolean notimeout = experiment.conduct(numberOfRepeats);
		
		out.println(experiment.toString() + " Method:" + ordering.toString());
		out.flush();
		
		return notimeout;
    }
    
    public void createALL(Module world, Command command, FileReporter rep) throws Err {
    	TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, new A4Options(A4Options.SatSolver.CNF));
		TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, new A4Options(A4Options.SatSolver.KK));
		TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, new A4Options(A4Options.SatSolver.DOT));
		TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, new A4Options(A4Options.SatSolver.VARS));
    }
}
